Nuprl Lemma : islocal-not-isrcv
0,22
postcript
pdf
k
:Knd. islocal(
k
) ~
isrcv(
k
)
latex
Definitions
x
:
A
.
B
(
x
)
,
b
,
t
T
,
Knd
,
islocal(
k
)
,
isrcv(
k
)
Lemmas
Knd
wf
origin
k:Knd. islocal(k) ~ 
isrcv(k) k:Knd. islocal(k) ~ isrcv(k) x:A. B(x)b
T